world-rename(rx;ra;rt;rainv;rtinv;w)
== <(i,x. vartype(i;rx(x)))
== ,(i,a. 1of(2of(w))(i,ra(a)))
== ,(l,tg. w.M(l,rt(tg)))
== ,(i,t,x. s(i;t).rx(x))
== ,(i,t. action-rename(rainv;rtinv;a(i;t)))
== ,(i,t. mapfilter(m.msg-rename(rtinv;m);m.isl(rtinv(mtag(m)));m(i;t)))
== ,(i.NullMachine)
== ,> 

latex

---

clarification:

world-rename(rx;ra;rt;rainv;rtinv;w)
== <(i,x. w-vartype(w; i; (rx(x))))
== ,(i,a. 1of(2of(w))(i,ra(a)))
== ,(l,tg. w.M(l,rt(tg)))
== ,(i,t,x. w-s(w; i; t; (rx(x))))
== ,(i,t. action-rename(rainv;rtinv;w-a(w; i; t)))
== ,(i,t. mapfilter(m.msg-rename(rtinv;m);m.isl(rtinv(mtag(m)));w-m(w; i; t)))
== ,(i.NullMachine)
== ,> 

latex

Definitions	vartype(i;x), 1of(t), 2of(t), w.M, s(i;t).x, action-rename(rainv;rtinv;a), a(i;t), mapfilter(f;P;L), msg-rename(rtinv;m), isl(x), f(a), mtag(m), m(i;t), <a,b>, x.A(x), NullMachine,
FDL editor aliases	world-rename